Effiziente Termersetzung

Projektleitung und Mitarbeiter

Mittelgeber :

Forschungsbericht : 1994-1996

Tel./ Fax.:

Projektbeschreibung

Auf Termersetzung basierende automatische Beweisverfahren werden auf effiziente Implementierungsmöglichkeiten hin untersucht. Dies umfaßt die Entwicklung von kritischen Paarkriterien und die Untersuchung von Strategien für Termvervollständigungsverfahren (modulo Assoziativität und Kommutuativität) und auch die Erweiterung von Termersetzungssysteme um eingebaute Datentypen. Im letzten Fall wird neben dem reinen Termersetzen auch das Auswerten von Termen mit vorgegebener Bedeutung unterstützt. In diesem Zusammenhang wird das Termersetzungslabor ReDuX entwickelt. ReDuX ist per ftp frei erhältlich.

Publikationen

INDEX HOME SUCHEN KONTAKT LINKS